(P:State(ds) -> Bool)
== ma{ds;
== ma{locl(a) : Outcome;
== ma{
;
== ma{a : P;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{a : p}
clarification:
(precondition a:Outcome(p) is
(P:State(ds) -> Bool)
== ma{ds;
== ma{locl(a) : p-outcome(p);
== ma{
;
== ma{a : P;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{
;
== ma{a : p}